\section{Agda} \label{sec:podstawy-agdy}
Agda \cite{agdafoundation} to zależnie typowany język programowania oraz wspomagacz dowodzenia \cite{agdawiki}. Agda jest oparta na Zunifikowanej Teorii Typów \cite{wikipedia-o-agdzie} autorstwa Zhaohui Luo \cite{unifiedtypetheory}, podobnej do Teorii Typów {\PerMartinLofDopelniacz}.
Składnia Agdy jest wzorowana na składni Haskell'a. 
\subsection{Definicja typów indukcyjnych} \label{subsection:definicja-typow-indukcyjnych}
Typu indukcyje (o sile wyrazu równoważnej (\ref{subsec:w-typy})) definiuje się przez podanie konstruktorów. Dla przykładu, definicja liczb naturalnych będąca równoważna podanej w (\ref{subsubsec:nat-konstr}) to
\input{agda-tex/Nat}
Słowo kluczowe \inlinecode{Data} oznacza definicję typu indukcyjnego. \inlinecode{Set zero} oznacza $\universe{0}$.
\inlinecode{0\#} to pierwszy konstruktor, \inlinecode{suc} to konstruktor wymagający $\nat$ jako argumentu.
Analogicznie można zdefiniować typ identycznosciowy (\ref{subsec:typ-identycznosciowy})

\input{agda-tex/IdTex}

Argumenty podane w nawiasach klamrowych \inlinecode{a : Level} i \inlinecode{A : Set a} to agumenty które są wnioskowane na podstawie innych argumentów (typ \inlinecode{A} jest wnioskowany na podstawie argumentu \inlinecode{x}, a  \inlinecode{a} na podstawie \inlinecode{A}). \inlinecode{a : Level} to indeks uniwersum (\ref{subsec:wszechswiaty}), typ jest zdefiniowany tak, żeby był używalny dla typów każdym uniwersum (zgdonie z Teorią Typów {\PerMartinLofDopelniacz} powinno się zdfiniować taki typ osobno dla każdego uniwersum, to jest obejście tego wymagania). Typ \inlinecode{Id} jest generowany na podstawie dwóch argumentów (``\texttt{A} $\rightarrow$ \texttt{A} $\rightarrow$ \texttt{Set a}''), ponieważ służy porównywaniu dwóch obiektów. Jedyny konstruktor typu to \inlinecode{refl}, który na podstawie jednego argumentu \inlinecode{x} tworzy instancję typu \inlinecode{Id x x}.
Poniżej definicji znajduje się twierdzenie o tym, że $0 = 0$ oraz nieprawdziwa hipoteza: $1 = 0$.
\subsection{Dowody}
Dowód to funckja z założeń w wypowiedzenie twierdzenia. Przykład podano w (\ref{section:przyklad-podstaw}). Reguła eliminacji dla typów zdefiniowanych jak w (\ref{subsection:definicja-typow-indukcyjnych}) jest przykryta słodzikiem w postaci dopasowania do wzorców, na przykład:
\input{agda-tex/Nat-double}
Funkcje zdefiniowane rekurencyjne muszą być udowadnialnie obliczalne w skończonym czasie, Agda dopuszcza rekurencję strukturalną \cite{Abel98foetus} \cite[strona ``Termination Checking'']{agda-doc}.
